free theorem

参考

関数がGenericに書かれているならば、それらの関数について一定の性質が満たされることが、（unit testとかで確認しなくても）保証される、という話です。具体的な型に落として関数を実装するのでなく、あえてGenericに書くことで得られる良い性質。tweet

何がfreeなん？

これってfunctor即の話？

それともFunctor則は例示なだけ？

定理

fmap :: (a -> b) -> F a -> F bは、

以下のような関数f、g、k、hが与えられたとき

code:hs

g . h = k . f

以下を満たす

code:hs

$map g . fmap h = fmap k . $map f

ここで、$mapはFに関する自然なmap

補題1

code:hs

fmap f = $map f

Functor則の1つ目と、free theoremから導出できる

補題2

code:hs

f . g = id . (f . g)

定理

code:hs

fmap f. fmap g = fmap (f . g)

Functor則の2つ目mrsekut.icon

証明

Theorems for free!に書いているらしい

割と大変っぽい

Functor則は、1つ目とfree theoremから2つ目を導出できる

code:hs

fmap id = id

fmap f . fmap g = fmap (f . g)

導出

https://gyazo.com/830db6c0e463c23342daec8794efc2ac

ここでも言及されていた

parametricだからこそ得られる性質である、的なことが書いてある

Generic型クラスとも凄く関連がありそうだけよくわからん